\begin{tabbing}
$\forall$\=$D$:Dsys, $i$:Id, $s_{1}$, $s_{2}$:M($i$).(timed)state, $k_{1}$, $k_{2}$:Knd, $v_{1}$:d{-}decl($D$;$i$)($k_{1}$),\+
\\[0ex]$v_{2}$:d{-}decl($D$;$i$)($k_{2}$), $m_{1}$:(\{$m$:M($i$).Msg$\mid$ source(mlnk($m$)) = $i$\}  List).
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ ($<$$s_{1}$, doact($k_{1}$;$v_{1}$), $m_{1}$$>$ = next{-}world{-}state($D$;$i$;$s_{2}$;$k_{2}$;$v_{2}$) $\in$ d{-}world{-}state($D$;$i$))
\\[0ex]$\Rightarrow$ \=\{$s_{1}$ = shift{-}state($\lambda$$x$.M($i$).ef($k_{2}$,$x$,read{-}state($s_{2}$),$v_{2}$)?$s_{2}$($x$))\+
\\[0ex]\& $k_{1}$ = $k_{2}$
\\[0ex]\& $v_{1}$ = $v_{2}$ $\in$ d{-}decl($D$;$i$)($k_{2}$)
\\[0ex]\& $m_{1}$ = filter($\lambda$$m$.source(mlnk($m$)) = $i$;M($i$).sends($k_{2}$,read{-}state($s_{2}$),$v_{2}$))\}
\-
\end{tabbing}